|
Q0 is Peter Andrews' formulation of the simply-typed lambda calculus, and provides a foundation for mathematics comparable to first-order logic plus set theory. It is a form of higher-order logic and closely related to the logics of the HOL theorem prover family. The theorem proving systems (TPS and ETPS ) are based on Q0. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.〔(The CADE-22 ATP System Competition (CASC-22) )〕 == Axioms of Q0 == The system has just five axioms, which can be stated as: (Axioms 2, 3, and 4 are axiom schemas—families of similar axioms. Instances of Axiom 2 and Axiom 3 vary only by the types of variables and constants, but instances of Axiom 4 can have any expression replacing A and B.) The subscripted "''o''" is the type symbol for boolean values, and subscripted "''i''" is the type symbol for individual (non-boolean) values. Sequences of these represent types of functions, and can include parentheses to distinguish different function types. Subscripted Greek letters such as α and β are syntactic variables for type symbols. Bold capital letters such as , , and are syntactic variables for WFFs, and bold lower case letters such as , are syntactic variables for variables. indicates syntactic substitution at all free occurrences. The only primitive constants are , denoting equality of members of each type α, and , denoting a description operator for individuals, the unique element of a set containing exactly one individual. The symbols λ and brackets ("(and " )") are syntax of the language. All other symbols are abbreviations for terms containing these, including quantifiers ∀ and ∃. In Axiom 4, must be free for in , meaning that the substitution does not cause any occurrences of free variables of to become bound in the result of the substitution. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Q zero」の詳細全文を読む スポンサード リンク
|